Report for no_context/loop4.c

1

extern void abort(void);  

2

3

extern void __assert_fail (const char *__assertion, const char *__file,  

4

      unsigned int __line, const char *__function)  

5

     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));  

6

extern void __assert_perror_fail (int __errnum, const char *__file,  

7

      unsigned int __line, const char *__function)  

8

     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));  

9

extern void __assert (const char *__assertion, const char *__file, int __line)  

10

     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));  

11

12

void reach_error() { ((void) sizeof ((0) ? 1 : 0), __extension__ ({ if (0) ; else __assert_fail ("0", "assert.h", 3, __extension__ __PRETTY_FUNCTION__); })); }  

13

extern void abort(void);  

14

void assume_abort_if_not(int cond) {  

15

  if(!cond) {abort();}  

16

}  

17

void __VERIFIER_assert(int cond) {  

18

  if (!(cond)) {  

19

      ERROR: {reach_error();abort();}  

20

  }  

21

  return;  

22

}  

23

int __VERIFIER_nondet_int();  

24

int main() {  

25

    int x,y;  

26

    x = 0;  

27

    y = 0;  

28

    while (1) {  

29

        if (x < 50) {  

30

            y++;  

31

        } else {  

32

            y--;  

33

        }  

34

        if (y < 0) break;  

35

        x++;  

36

    }  

37

    __VERIFIER_assert(x == 100);  

38

    return 0;  

39

}